Nuprl Lemma : es-locl-trans-test
11,40
postcript
pdf
es
:ES,
a
,
b
,
c
,
d
,
e
,
f
:E.
a
loc
b
b
loc
c
(
c
<loc
d
)
d
loc
e
e
loc
f
a
loc
f
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
ES
,
E
,
e
loc
e'
,
(
e
<loc
e'
)
,
strong-subtype(
A
;
B
)
,
P
Q
Lemmas
es-locl
wf
,
es-le
wf
,
es-E
wf
,
event
system
wf
,
es-le
transitivity
,
es-locl
transitivity1
,
es-locl
transitivity2
,
es-le
weakening
origin
es:ES, a, b, c, d, e, f:E.
loc b 
b loc c (c <loc d) d loc e e loc f a loc f es:ES, a, b, c, d, e, f:E.
loc b b loc c (c <loc d) d loc e e loc f a loc f 
T
B(x)x:A. B(x)loc e' Q